Bob is round. Charlie is not cold. Charlie is furry. Charlie is red. Erin is blue. Erin is red. Erin is not round. If something is cold and red then it is not furry. All furry things are young. If something is young and green then it is not blue. If something is red then it is not cold. If Bob is young then Bob is not blue. All red, young things are green. If something is blue and furry then it is round. If something is blue and not furry then it is not round.
Bob is round.
("Bob" "is" "round" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not round.
("Erin" "is" "round" "-")
If something is cold and red then it is not furry.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "-"))
All furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is young and green then it is not blue.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "-"))
If something is red then it is not cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "-"))
If Bob is young then Bob is not blue.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "blue" "-"))
All red, young things are green.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is blue and furry then it is round.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If something is blue and not furry then it is not round.
((("something" "is" "blue" "+") ("something" "is" "furry" "~")) -> ("something" "is" "round" "-"))
Charlie is not cold.
True
1
proof
[(triple2 OR ((triple4) -> rule4))]
("Charlie" "is" "cold" "-")
triple2
((triple4) -> (rule4 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Bob is not round.
False
1
inv-proof
[(triple1)]
("Bob" "is" "round" "-")
triple1
Erin is not cold.
True
2
proof
[(((triple6) -> rule4))]
("Erin" "is" "cold" "-")
((triple6) -> (rule4 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is cold.
False
2
inv-proof
[(((triple6) -> rule4))]
("Erin" "is" "cold" "+")
((triple6) -> (rule4 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Charlie is green.
True
4
proof
[(((triple4 ((triple3) -> rule2)) -> rule6))]
("Charlie" "is" "green" "+")
((triple4 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not green.
False
4
inv-proof
[(((triple4 ((triple3) -> rule2)) -> rule6))]
("Charlie" "is" "green" "-")
((triple4 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not blue.
True
7
proof
[(((((triple3) -> rule2) ((triple4 ((triple3) -> rule2)) -> rule6)) -> rule3))]
("Charlie" "is" "blue" "-")
((((triple3) -> (rule2 % int3)) ((triple4 ((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is blue.
False
7
inv-proof
[(((((triple3) -> rule2) ((triple4 ((triple3) -> rule2)) -> rule6)) -> rule3))]
("Charlie" "is" "blue" "+")
((((triple3) -> (rule2 % int3)) ((triple4 ((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "round" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "young" "+")
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "green" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "young" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is round.[(triple1)] Charlie is furry.[(triple3)] Charlie is not cold.[(triple2 OR ((triple4) -> rule4))] Charlie is red.[(triple4)] Erin is blue.[(triple5)] Erin is not round.[(triple7)] Erin is red.[(triple6)] @1: Charlie is young.[(((triple3) -> rule2))] Erin is not cold.[(((triple6) -> rule4))] @2: Charlie is green.[(((triple4 ((triple3) -> rule2)) -> rule6))] @3: Charlie is not blue.[(((((triple3) -> rule2) ((triple4 ((triple3) -> rule2)) -> rule6)) -> rule3))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
((triple4) -> (rule4 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is not round.
("Erin" "is" "round" "-")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
((triple3) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
((triple6) -> (rule4 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple4 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not blue.
("Charlie" "is" "blue" "-")
((((triple3) -> (rule2 % int3)) ((triple4 ((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3