Bob is big. Bob is nice. Charlie is big. Charlie is blue. Charlie is nice. Charlie is round. Charlie is smart. Harry is big. Harry is kind. Harry is nice. Kind, blue people are smart. Big, blue people are kind. If someone is nice then they are blue. If someone is round and blue then they are rough. All round people are rough. All nice people are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Kind, blue people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Big, blue people are kind.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is nice then they are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is round and blue then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
All round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Charlie is big.
True
1
proof
[(triple3 OR ((triple5) -> rule6))]
("Charlie" "is" "big" "+")
triple3
((triple5) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not round.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "round" "-")
triple6
Charlie is rough.
True
2
proof
[(((triple6) -> rule5) OR ((triple6 triple4) -> rule4) OR ((triple6 ((triple5) -> rule3)) -> rule4))]
("Charlie" "is" "rough" "+")
((triple6) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple6 triple4) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple6 ((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not rough.
False
2
inv-proof
[(((triple6) -> rule5) OR ((triple6 triple4) -> rule4) OR ((triple6 ((triple5) -> rule3)) -> rule4))]
("Charlie" "is" "rough" "-")
((triple6) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple6 triple4) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple6 ((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "rough" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "rough" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Bob is big.[(triple1 OR ((triple2) -> rule6))] Bob is nice.[(triple2)] Charlie is big.[(triple3 OR ((triple5) -> rule6))] Charlie is blue.[(triple4 OR ((triple5) -> rule3))] Charlie is nice.[(triple5)] Charlie is round.[(triple6)] Charlie is smart.[(triple7 OR ((((triple3 triple4) -> rule2) triple4) -> rule1) OR ((((triple3 triple4) -> rule2) ((triple5) -> rule3)) -> rule1) OR ((((triple3 ((triple5) -> rule3)) -> rule2) triple4) -> rule1) OR ((((((triple5) -> rule6) triple4) -> rule2) triple4) -> rule1) OR ((((triple3 ((triple5) -> rule3)) -> rule2) ((triple5) -> rule3)) -> rule1) OR ((((((triple5) -> rule6) triple4) -> rule2) ((triple5) -> rule3)) -> rule1) OR ((((((triple5) -> rule6) ((triple5) -> rule3)) -> rule2) triple4) -> rule1) OR ((((((triple5) -> rule6) ((triple5) -> rule3)) -> rule2) ((triple5) -> rule3)) -> rule1))] Harry is big.[(triple8 OR ((triple10) -> rule6))] Harry is kind.[(triple9 OR ((triple8 ((triple10) -> rule3)) -> rule2) OR ((((triple10) -> rule6) ((triple10) -> rule3)) -> rule2))] Harry is nice.[(triple10)] @1: Bob is blue.[(((triple2) -> rule3))] Charlie is kind.[(((triple3 triple4) -> rule2) OR ((triple3 ((triple5) -> rule3)) -> rule2) OR ((((triple5) -> rule6) triple4) -> rule2) OR ((((triple5) -> rule6) ((triple5) -> rule3)) -> rule2))] Charlie is rough.[(((triple6) -> rule5) OR ((triple6 triple4) -> rule4) OR ((triple6 ((triple5) -> rule3)) -> rule4))] Harry is blue.[(((triple10) -> rule3))] @2: Bob is kind.[(((triple1 ((triple2) -> rule3)) -> rule2) OR ((((triple2) -> rule6) ((triple2) -> rule3)) -> rule2))] Harry is smart.[(((triple9 ((triple10) -> rule3)) -> rule1) OR ((((triple8 ((triple10) -> rule3)) -> rule2) ((triple10) -> rule3)) -> rule1) OR ((((((triple10) -> rule6) ((triple10) -> rule3)) -> rule2) ((triple10) -> rule3)) -> rule1))] @3: Bob is smart.[(((((triple1 ((triple2) -> rule3)) -> rule2) ((triple2) -> rule3)) -> rule1) OR ((((((triple2) -> rule6) ((triple2) -> rule3)) -> rule2) ((triple2) -> rule3)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
((triple5) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
((triple5) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
((((triple3 triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple3 triple4) -> (rule2 % int3)) ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((triple3 ((triple5) -> (rule3 % int3))) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((((triple5) -> (rule6 % int3)) triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple3 ((triple5) -> (rule3 % int3))) -> (rule2 % int2)) ((triple5) -> (rule3 % int3))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((((triple5) -> (rule6 % int4)) triple4) -> (rule2 % int3)) ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
((((((triple5) -> (rule6 % int4)) ((triple5) -> (rule3 % int3))) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
((((((triple5) -> (rule6 % int4)) ((triple5) -> (rule3 % int3))) -> (rule2 % int2)) ((triple5) -> (rule3 % int3))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple10) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple9
((triple8 ((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple10) -> (rule6 % int3)) ((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3 triple4) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple3 ((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple5) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple5) -> (rule6 % int3)) ((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple6) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple6 triple4) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple6 ((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((triple10) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple1 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple2) -> (rule6 % int3)) ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((triple9 ((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple8 ((triple10) -> (rule3 % int3))) -> (rule2 % int2)) ((triple10) -> (rule3 % int3))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple10) -> (rule6 % int4)) ((triple10) -> (rule3 % int3))) -> (rule2 % int2)) ((triple10) -> (rule3 % int3))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1 ((triple2) -> (rule3 % int3))) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((triple2) -> (rule6 % int4)) ((triple2) -> (rule3 % int3))) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4