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