Bob is not big. Bob is not cold. Bob is quiet. Bob is not round. Bob is not white. Bob is young. Dave is big. Dave is cold. Dave is quiet. Dave is round. Dave is not smart. Dave is white. Dave is young. Harry is not round. Harry is smart. Harry is young. If something is young and not quiet then it is not white. All white things are young. If something is quiet and not young then it is not smart. If something is white then it is not smart. If something is smart then it is cold. All white, quiet things are cold. If something is big and not quiet then it is round. All smart, big things are round.
Bob is not big.
("Bob" "is" "big" "-")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not round.
("Bob" "is" "round" "-")
Bob is not white.
("Bob" "is" "white" "-")
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is not round.
("Harry" "is" "round" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is young and not quiet then it is not white.
((("something" "is" "young" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "white" "-"))
All white things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is quiet and not young then it is not smart.
((("something" "is" "quiet" "+") ("something" "is" "young" "~")) -> ("something" "is" "smart" "-"))
If something is white then it is not smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "-"))
If something is smart then it is cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All white, quiet things are cold.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If something is big and not quiet then it is round.
((("something" "is" "big" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "round" "+"))
All smart, big things are round.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Dave is not smart.
True
1
proof
[(triple11 OR ((triple12) -> rule4))]
("Dave" "is" "smart" "-")
triple11
((triple12) -> (rule4 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Bob is not quiet.
False
1
inv-proof
[(triple3)]
("Bob" "is" "quiet" "-")
triple3
Harry is cold.
True
2
proof
[(((triple15) -> rule5))]
("Harry" "is" "cold" "+")
((triple15) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple15) -> rule5))]
("Harry" "is" "cold" "-")
((triple15) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is not big.[(triple1)] Bob is not cold.[(triple2)] Bob is not round.[(triple4)] Bob is not white.[(triple5)] Bob is quiet.[(triple3)] Bob is young.[(triple6)] Dave is big.[(triple7)] Dave is cold.[(triple8 OR ((triple12 triple9) -> rule6))] Dave is not smart.[(triple11 OR ((triple12) -> rule4))] Dave is quiet.[(triple9)] Dave is round.[(triple10)] Dave is white.[(triple12)] Dave is young.[(triple13 OR ((triple12) -> rule2))] Harry is not round.[(triple14)] Harry is smart.[(triple15)] Harry is young.[(triple16)] @1: Harry is cold.[(((triple15) -> rule5))]
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is not cold.
("Bob" "is" "cold" "-")
triple2
Bob is not round.
("Bob" "is" "round" "-")
triple4
Bob is not white.
("Bob" "is" "white" "-")
triple5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple6
Dave is big.
("Dave" "is" "big" "+")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
triple8
((triple12 triple9) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not smart.
("Dave" "is" "smart" "-")
triple11
((triple12) -> (rule4 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple12
Dave is young.
("Dave" "is" "young" "+")
triple13
((triple12) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Harry is not round.
("Harry" "is" "round" "-")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Harry is cold.
("Harry" "is" "cold" "+")
((triple15) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1