Bob is big. Bob is quiet. Bob is red. Bob is young. Dave is red. Dave is rough. Dave is round. If Dave is red and Dave is big then Dave is quiet. All quiet, young people are smart. All round, rough people are red. Rough people are smart. All red people are quiet. All big, young people are round.
Bob is big.
("Bob" "is" "big" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
If Dave is red and Dave is big then Dave is quiet.
((("Dave" "is" "red" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "quiet" "+"))
All quiet, young people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All round, rough people are red.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
Rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
All big, young people are round.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Dave is round.
True
1
proof
[(triple7)]
("Dave" "is" "round" "+")
triple7
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Dave is smart.
True
2
proof
[(((triple6) -> rule4))]
("Dave" "is" "smart" "+")
((triple6) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Bob is not round.
False
3
inv-proof
[(((triple1 triple4) -> rule6))]
("Bob" "is" "round" "-")
((triple1 triple4) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is quiet.[(triple2 OR ((triple3) -> rule5))] Bob is red.[(triple3)] Bob is young.[(triple4)] Dave is red.[(triple5 OR ((triple7 triple6) -> rule3))] Dave is rough.[(triple6)] Dave is round.[(triple7)] @1: Bob is round.[(((triple1 triple4) -> rule6))] Bob is smart.[(((triple2 triple4) -> rule2) OR ((((triple3) -> rule5) triple4) -> rule2))] Dave is quiet.[(((triple5) -> rule5) OR ((((triple7 triple6) -> rule3)) -> rule5))] Dave is smart.[(((triple6) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
((triple3) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple7 triple6) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
Bob is round.
("Bob" "is" "round" "+")
((triple1 triple4) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple2 triple4) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple3) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple5) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple7 triple6) -> (rule3 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple6) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1