Anne is blue. Charlie is red. Fiona is cold. Harry is round. If something is blue and red then it is big. If something is smart then it is cold. All red things are big. If Charlie is red and Charlie is big then Charlie is blue. Big things are smart. All nice things are big.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is blue and red then it is big.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is smart then it is cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If Charlie is red and Charlie is big then Charlie is blue.
((("Charlie" "is" "red" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "blue" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Fiona is cold.
True
1
proof
[(triple3)]
("Fiona" "is" "cold" "+")
triple3
Charlie is not red.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "red" "-")
triple2
Charlie is big.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "big" "+")
((triple2) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "big" "-")
((triple2) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("Charlie" "is" "smart" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not blue.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule4))]
("Charlie" "is" "blue" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is cold.
True
4
proof
[(((((((triple2) -> rule3)) -> rule5)) -> rule2))]
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not cold.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule5)) -> rule2))]
("Charlie" "is" "cold" "-")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Anne is not smart.
Unknown
inv-rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Anne" "is" "smart" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not cold.
Unknown
inv-rconc
[@3: Harry is cold.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule1 <- FAIL)]]
("Harry" "is" "cold" "-")
Anne is cold.
Unknown
rconc
[@3: Anne is cold.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule1 <- FAIL)]]
("Anne" "is" "cold" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is blue.[(triple1)] Charlie is red.[(triple2)] Fiona is cold.[(triple3)] Harry is round.[(triple4)] @1: Charlie is big.[(((triple2) -> rule3))] @2: Charlie is blue.[(((triple2 ((triple2) -> rule3)) -> rule4))] Charlie is smart.[(((((triple2) -> rule3)) -> rule5))] @3: Charlie is cold.[(((((((triple2) -> rule3)) -> rule5)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3