Bob is cold. Bob is furry. Bob is nice. Bob is quiet. Bob is rough. Bob is young. Charlie is cold. Charlie is furry. Charlie is quiet. Fiona is cold. Fiona is nice. Harry is cold. Harry is furry. Harry is nice. Harry is quiet. Harry is young. All blue, young people are nice. If someone is cold then they are rough. Quiet people are furry. If someone is young then they are cold. If someone is quiet and rough then they are blue. If someone is rough and quiet then they are blue.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
All blue, young people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold then they are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
Quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If someone is young then they are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is quiet and rough then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough and quiet then they are blue.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Bob is furry.
True
1
proof
[(triple2 OR ((triple4) -> rule3))]
("Bob" "is" "furry" "+")
triple2
((triple4) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Harry is not furry.
False
1
inv-proof
[(triple13 OR ((triple15) -> rule3))]
("Harry" "is" "furry" "-")
triple13
((triple15) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Fiona is rough.
True
2
proof
[(((triple10) -> rule2))]
("Fiona" "is" "rough" "+")
((triple10) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple7) -> rule2))]
("Charlie" "is" "rough" "-")
((triple7) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Harry is blue.
True
4
proof
[(((triple15 ((triple12) -> rule2)) -> rule5) OR ((((triple12) -> rule2) triple15) -> rule6) OR ((triple15 ((((triple16) -> rule4)) -> rule2)) -> rule5) OR ((((((triple16) -> rule4)) -> rule2) triple15) -> rule6))]
("Harry" "is" "blue" "+")
((triple15 ((triple12) -> (rule2 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple12) -> (rule2 % int2)) triple15) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple15 ((((triple16) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((((triple16) -> (rule4 % int3))) -> (rule2 % int2)) triple15) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not blue.
False
4
inv-proof
[(((triple15 ((triple12) -> rule2)) -> rule5) OR ((((triple12) -> rule2) triple15) -> rule6) OR ((triple15 ((((triple16) -> rule4)) -> rule2)) -> rule5) OR ((((((triple16) -> rule4)) -> rule2) triple15) -> rule6))]
("Harry" "is" "blue" "-")
((triple15 ((triple12) -> (rule2 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple12) -> (rule2 % int2)) triple15) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple15 ((((triple16) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((((triple16) -> (rule4 % int3))) -> (rule2 % int2)) triple15) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "furry" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "+")
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Bob is cold.[(triple1 OR ((triple6) -> rule4))] Bob is furry.[(triple2 OR ((triple4) -> rule3))] Bob is nice.[(triple3 OR ((((triple4 triple5) -> rule5) triple6) -> rule1) OR ((((triple5 triple4) -> rule6) triple6) -> rule1) OR ((((triple4 ((triple1) -> rule2)) -> rule5) triple6) -> rule1) OR ((((((triple1) -> rule2) triple4) -> rule6) triple6) -> rule1) OR ((((triple4 ((((triple6) -> rule4)) -> rule2)) -> rule5) triple6) -> rule1) OR ((((((((triple6) -> rule4)) -> rule2) triple4) -> rule6) triple6) -> rule1))] Bob is quiet.[(triple4)] Bob is rough.[(triple5 OR ((triple1) -> rule2) OR ((((triple6) -> rule4)) -> rule2))] Bob is young.[(triple6)] Charlie is cold.[(triple7)] Charlie is furry.[(triple8 OR ((triple9) -> rule3))] Charlie is quiet.[(triple9)] Fiona is cold.[(triple10)] Fiona is nice.[(triple11)] Harry is cold.[(triple12 OR ((triple16) -> rule4))] Harry is furry.[(triple13 OR ((triple15) -> rule3))] Harry is nice.[(triple14 OR ((((triple15 ((triple12) -> rule2)) -> rule5) triple16) -> rule1) OR ((((((triple12) -> rule2) triple15) -> rule6) triple16) -> rule1) OR ((((triple15 ((((triple16) -> rule4)) -> rule2)) -> rule5) triple16) -> rule1) OR ((((((((triple16) -> rule4)) -> rule2) triple15) -> rule6) triple16) -> rule1))] Harry is quiet.[(triple15)] Harry is young.[(triple16)] @1: Bob is blue.[(((triple4 triple5) -> rule5) OR ((triple5 triple4) -> rule6) OR ((triple4 ((triple1) -> rule2)) -> rule5) OR ((((triple1) -> rule2) triple4) -> rule6) OR ((triple4 ((((triple6) -> rule4)) -> rule2)) -> rule5) OR ((((((triple6) -> rule4)) -> rule2) triple4) -> rule6))] Charlie is rough.[(((triple7) -> rule2))] Fiona is rough.[(((triple10) -> rule2))] Harry is rough.[(((triple12) -> rule2) OR ((((triple16) -> rule4)) -> rule2))] @2: Charlie is blue.[(((triple9 ((triple7) -> rule2)) -> rule5) OR ((((triple7) -> rule2) triple9) -> rule6))] Harry is blue.[(((triple15 ((triple12) -> rule2)) -> rule5) OR ((((triple12) -> rule2) triple15) -> rule6) OR ((triple15 ((((triple16) -> rule4)) -> rule2)) -> rule5) OR ((((((triple16) -> rule4)) -> rule2) triple15) -> rule6))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple6) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple4) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((((triple4 triple5) -> (rule5 % int2)) triple6) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple5 triple4) -> (rule6 % int2)) triple6) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple4 ((triple1) -> (rule2 % int3))) -> (rule5 % int2)) triple6) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((((triple1) -> (rule2 % int3)) triple4) -> (rule6 % int2)) triple6) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((triple4 ((((triple6) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple6) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
((((((((triple6) -> (rule4 % int4))) -> (rule2 % int3)) triple4) -> (rule6 % int2)) triple6) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
((triple9) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Fiona is cold.
("Fiona" "is" "cold" "+")
triple10
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
((triple16) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple13
((triple15) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple14
((((triple15 ((triple12) -> (rule2 % int3))) -> (rule5 % int2)) triple16) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((triple12) -> (rule2 % int3)) triple15) -> (rule6 % int2)) triple16) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple15 ((((triple16) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple16) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
((((((((triple16) -> (rule4 % int4))) -> (rule2 % int3)) triple15) -> (rule6 % int2)) triple16) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Bob is blue.
("Bob" "is" "blue" "+")
((triple4 triple5) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple5 triple4) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple4 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple1) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((triple4 ((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((triple6) -> (rule4 % int3))) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple7) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple10) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple12) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple16) -> (rule4 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple9 ((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple7) -> (rule2 % int2)) triple9) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((triple15 ((triple12) -> (rule2 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple12) -> (rule2 % int2)) triple15) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple15 ((((triple16) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((((triple16) -> (rule4 % int3))) -> (rule2 % int2)) triple15) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3