Charlie is blue. Charlie is red. Dave is furry. Dave is nice. Dave is red. Dave is white. Fiona is not blue. Fiona is furry. Fiona is nice. Fiona is young. If someone is white and nice then they are not young. All cold people are furry. Blue people are furry. All young people are cold. If someone is furry and nice then they are cold. If someone is furry then they are nice. If Charlie is not blue then Charlie is white. If Dave is young and Dave is red then Dave is cold.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is not blue.
("Fiona" "is" "blue" "-")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is white and nice then they are not young.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "-"))
All cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry and nice then they are cold.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry then they are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is not blue then Charlie is white.
((("Charlie" "is" "blue" "~")) -> ("Charlie" "is" "white" "+"))
If Dave is young and Dave is red then Dave is cold.
((("Dave" "is" "young" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "cold" "+"))
Dave is red.
True
1
proof
[(triple5)]
("Dave" "is" "red" "+")
triple5
Charlie is not red.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "red" "-")
triple2
Charlie is furry.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple10) -> rule4) OR ((triple8 triple9) -> rule5) OR ((triple8 ((triple8) -> rule6)) -> rule5))]
("Fiona" "is" "cold" "-")
((triple10) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple8 triple9) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple8 ((triple8) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Charlie is nice.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("Charlie" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not nice.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("Charlie" "is" "nice" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is cold.
True
6
proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule6)) -> rule5))]
("Charlie" "is" "cold" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not cold.
False
6
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule6)) -> rule5))]
("Charlie" "is" "cold" "-")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Charlie is blue.[(triple1)] Charlie is red.[(triple2)] Dave is furry.[(triple3)] Dave is nice.[(triple4 OR ((triple3) -> rule6))] Dave is red.[(triple5)] Dave is white.[(triple6)] Fiona is furry.[(triple8 OR ((((triple10) -> rule4)) -> rule2))] Fiona is nice.[(triple9 OR ((triple8) -> rule6) OR ((((((triple10) -> rule4)) -> rule2)) -> rule6))] Fiona is not blue.[(triple7)] Fiona is young.[(triple10)] @1: Charlie is furry.[(((triple1) -> rule3))] Dave is cold.[(((triple3 triple4) -> rule5) OR ((triple3 ((triple3) -> rule6)) -> rule5))] Dave is not young.[(((triple6 triple4) -> rule1) OR ((triple6 ((triple3) -> rule6)) -> rule1))] Fiona is cold.[(((triple10) -> rule4) OR ((triple8 triple9) -> rule5) OR ((triple8 ((triple8) -> rule6)) -> rule5))] @2: Charlie is nice.[(((((triple1) -> rule3)) -> rule6))] @3: Charlie is cold.[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule6)) -> rule5))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
((triple3) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
((((triple10) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
((triple8) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((((triple10) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is not blue.
("Fiona" "is" "blue" "-")
triple7
Fiona is young.
("Fiona" "is" "young" "+")
triple10
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple3 triple4) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple3 ((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not young.
("Dave" "is" "young" "-")
((triple6 triple4) -> (rule1 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
((triple6 ((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple10) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple8 triple9) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple8 ((triple8) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3