Bob is green. Bob is rough. Charlie is blue. Erin is furry. Erin is green. Fiona is blue. Fiona is furry. Fiona is rough. Fiona is smart. Fiona is white. All white things are furry. Furry, rough things are cold. Cold things are blue. If something is green then it is white. If Erin is smart then Erin is white. Blue things are smart.
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
All white things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Furry, rough things are cold.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is green then it is white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If Erin is smart then Erin is white.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "white" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Fiona is rough.
True
1
proof
[(triple8)]
("Fiona" "is" "rough" "+")
triple8
Erin is not furry.
False
1
inv-proof
[(triple4 OR ((((triple5) -> rule4)) -> rule1))]
("Erin" "is" "furry" "-")
triple4
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Charlie is smart.
True
2
proof
[(((triple3) -> rule6))]
("Charlie" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "white" "-")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
True
3
proof
[(((((triple1) -> rule4)) -> rule1))]
("Bob" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule1))]
("Bob" "is" "furry" "-")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is cold.
True
5
proof
[(((((((triple1) -> rule4)) -> rule1) triple2) -> rule2))]
("Bob" "is" "cold" "+")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not cold.
False
5
inv-proof
[(((((((triple1) -> rule4)) -> rule1) triple2) -> rule2))]
("Bob" "is" "cold" "-")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is blue.
True
6
proof
[(((((((((triple1) -> rule4)) -> rule1) triple2) -> rule2)) -> rule3))]
("Bob" "is" "blue" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not blue.
False
6
inv-proof
[(((((((((triple1) -> rule4)) -> rule1) triple2) -> rule2)) -> rule3))]
("Bob" "is" "blue" "-")
((((((((triple1) -> (rule4 % int4))) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is smart.
True
7
proof
[(((((((((((triple1) -> rule4)) -> rule1) triple2) -> rule2)) -> rule3)) -> rule6))]
("Bob" "is" "smart" "+")
((((((((((triple1) -> (rule4 % int5))) -> (rule1 % int4)) triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Bob is not smart.
False
7
inv-proof
[(((((((((((triple1) -> rule4)) -> rule1) triple2) -> rule2)) -> rule3)) -> rule6))]
("Bob" "is" "smart" "-")
((((((((((triple1) -> (rule4 % int5))) -> (rule1 % int4)) triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Charlie is not furry.
Unknown
inv-rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Charlie" "is" "furry" "-")
Erin is blue.
Unknown
rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Erin" "is" "blue" "+")
Erin is not smart.
Unknown
inv-rconc
[@3: Erin is smart.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule2 <- FAIL)]]
("Erin" "is" "smart" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "cold" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "cold" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Bob is green.[(triple1)] Bob is rough.[(triple2)] Charlie is blue.[(triple3)] Erin is furry.[(triple4 OR ((((triple5) -> rule4)) -> rule1))] Erin is green.[(triple5)] Fiona is blue.[(triple6 OR ((((triple7 triple8) -> rule2)) -> rule3) OR ((((((triple10) -> rule1) triple8) -> rule2)) -> rule3))] Fiona is furry.[(triple7 OR ((triple10) -> rule1))] Fiona is rough.[(triple8)] Fiona is smart.[(triple9 OR ((triple6) -> rule6) OR ((((((triple7 triple8) -> rule2)) -> rule3)) -> rule6) OR ((((((((triple10) -> rule1) triple8) -> rule2)) -> rule3)) -> rule6))] Fiona is white.[(triple10)] @1: Bob is white.[(((triple1) -> rule4))] Charlie is smart.[(((triple3) -> rule6))] Erin is white.[(((triple5) -> rule4))] Fiona is cold.[(((triple7 triple8) -> rule2) OR ((((triple10) -> rule1) triple8) -> rule2))] @2: Bob is furry.[(((((triple1) -> rule4)) -> rule1))] @3: Bob is cold.[(((((((triple1) -> rule4)) -> rule1) triple2) -> rule2))] @4: Bob is blue.[(((((((((triple1) -> rule4)) -> rule1) triple2) -> rule2)) -> rule3))] @5: Bob is smart.[(((((((((((triple1) -> rule4)) -> rule1) triple2) -> rule2)) -> rule3)) -> rule6))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
((((triple7 triple8) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((((triple10) -> (rule1 % int3)) triple8) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
((triple10) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
Fiona is smart.
("Fiona" "is" "smart" "+")
triple9
((triple6) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((((triple7 triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((((((triple10) -> (rule1 % int4)) triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple5) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple7 triple8) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple10) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
((((((((((triple1) -> (rule4 % int5))) -> (rule1 % int4)) triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5