Bob is big. Bob is kind. Dave is big. Dave is cold. Dave is kind. Dave is nice. Dave is quiet. Gary is blue. Harry is blue. Harry is kind. Harry is nice. Harry is quiet. Kind things are nice. Big things are quiet. If something is big and cold then it is quiet. Blue, nice things are young. If something is nice and young then it is blue. If something is nice and kind then it is young.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is big and cold then it is quiet.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Blue, nice things are young.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is nice and young then it is blue.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is nice and kind then it is young.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Dave is not nice.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule1))]
("Dave" "is" "nice" "-")
triple6
((triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Harry is young.
True
3
proof
[(((triple11 triple10) -> rule6) OR ((triple9 triple11) -> rule4) OR ((triple9 ((triple10) -> rule1)) -> rule4) OR ((((triple10) -> rule1) triple10) -> rule6))]
("Harry" "is" "young" "+")
((triple11 triple10) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple9 triple11) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple9 ((triple10) -> (rule1 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple10) -> (rule1 % int2)) triple10) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Bob is not nice.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "nice" "-")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule6))]
("Bob" "is" "young" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not young.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule6))]
("Bob" "is" "young" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
True
7
proof
[(((((triple2) -> rule1) ((((triple2) -> rule1) triple2) -> rule6)) -> rule5))]
("Bob" "is" "blue" "+")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3)) triple2) -> (rule6 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not blue.
False
7
inv-proof
[(((((triple2) -> rule1) ((((triple2) -> rule1) triple2) -> rule6)) -> rule5))]
("Bob" "is" "blue" "-")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3)) triple2) -> (rule6 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Gary is not young.
Unknown
inv-rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is quiet.
Unknown
rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "nice" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is kind.[(triple2)] Dave is big.[(triple3)] Dave is cold.[(triple4)] Dave is kind.[(triple5)] Dave is nice.[(triple6 OR ((triple5) -> rule1))] Dave is quiet.[(triple7 OR ((triple3) -> rule2) OR ((triple3 triple4) -> rule3))] Gary is blue.[(triple8)] Harry is blue.[(triple9 OR ((triple11 ((triple11 triple10) -> rule6)) -> rule5) OR ((((triple10) -> rule1) ((triple11 triple10) -> rule6)) -> rule5) OR ((triple11 ((((triple10) -> rule1) triple10) -> rule6)) -> rule5) OR ((((triple10) -> rule1) ((((triple10) -> rule1) triple10) -> rule6)) -> rule5))] Harry is kind.[(triple10)] Harry is nice.[(triple11 OR ((triple10) -> rule1))] Harry is quiet.[(triple12)] @1: Bob is nice.[(((triple2) -> rule1))] Bob is quiet.[(((triple1) -> rule2))] Dave is young.[(((triple6 triple5) -> rule6) OR ((((triple5) -> rule1) triple5) -> rule6))] Harry is young.[(((triple11 triple10) -> rule6) OR ((triple9 triple11) -> rule4) OR ((triple9 ((triple10) -> rule1)) -> rule4) OR ((((triple10) -> rule1) triple10) -> rule6))] @2: Bob is young.[(((((triple2) -> rule1) triple2) -> rule6))] Dave is blue.[(((triple6 ((triple6 triple5) -> rule6)) -> rule5) OR ((((triple5) -> rule1) ((triple6 triple5) -> rule6)) -> rule5) OR ((triple6 ((((triple5) -> rule1) triple5) -> rule6)) -> rule5) OR ((((triple5) -> rule1) ((((triple5) -> rule1) triple5) -> rule6)) -> rule5))] @3: Bob is blue.[(((((triple2) -> rule1) ((((triple2) -> rule1) triple2) -> rule6)) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
((triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
((triple3) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple3 triple4) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
((triple11 ((triple11 triple10) -> (rule6 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple10) -> (rule1 % int3)) ((triple11 triple10) -> (rule6 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((triple11 ((((triple10) -> (rule1 % int3)) triple10) -> (rule6 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple10) -> (rule1 % int3)) ((((triple10) -> (rule1 % int3)) triple10) -> (rule6 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
((triple10) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple6 triple5) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple5) -> (rule1 % int2)) triple5) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((triple11 triple10) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple9 triple11) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple9 ((triple10) -> (rule1 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple10) -> (rule1 % int2)) triple10) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((triple6 ((triple6 triple5) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple6 triple5) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((triple6 ((((triple5) -> (rule1 % int3)) triple5) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((triple5) -> (rule1 % int3)) ((((triple5) -> (rule1 % int3)) triple5) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3)) triple2) -> (rule6 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3