Bob is red. Bob is round. Dave is kind. Dave is red. Dave is young. Harry is big. Harry is quiet. Harry is rough. Harry is round. Harry is young. Round people are red. All round, rough people are quiet. All young people are round.
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
Round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
All round, rough people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Harry is rough.
True
1
proof
[(triple8)]
("Harry" "is" "rough" "+")
triple8
Bob is not red.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule1))]
("Bob" "is" "red" "-")
triple1
((triple2) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is red.
True
2
proof
[(((triple9) -> rule1) OR ((((triple10) -> rule3)) -> rule1))]
("Harry" "is" "red" "+")
((triple9) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Dave is not round.
False
2
inv-proof
[(((triple5) -> rule3))]
("Dave" "is" "round" "-")
((triple5) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "quiet" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is red.[(triple1 OR ((triple2) -> rule1))] Bob is round.[(triple2)] Dave is kind.[(triple3)] Dave is red.[(triple4 OR ((((triple5) -> rule3)) -> rule1))] Dave is young.[(triple5)] Harry is big.[(triple6)] Harry is quiet.[(triple7 OR ((triple9 triple8) -> rule2) OR ((((triple10) -> rule3) triple8) -> rule2))] Harry is rough.[(triple8)] Harry is round.[(triple9 OR ((triple10) -> rule3))] Harry is young.[(triple10)] @1: Dave is round.[(((triple5) -> rule3))] Harry is red.[(((triple9) -> rule1) OR ((((triple10) -> rule3)) -> rule1))]
Bob is red.
("Bob" "is" "red" "+")
triple1
((triple2) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
((triple9 triple8) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple10) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
((triple10) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple10
Dave is round.
("Dave" "is" "round" "+")
((triple5) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple9) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2