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