Charlie is big. Erin is green. Fiona is quiet. If something is nice then it is green. If Charlie is nice then Charlie is green. Quiet things are cold. All green things are blue. If something is quiet then it is green. Blue, cold things are big. All blue things are nice. If something is quiet and blue then it is nice.
Charlie is big.
("Charlie" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If Charlie is nice then Charlie is green.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "green" "+"))
Quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Blue, cold things are big.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is quiet and blue then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Erin is not green.
False
1
inv-proof
[(triple2)]
("Erin" "is" "green" "-")
triple2
Fiona is cold.
True
2
proof
[(((triple3) -> rule3))]
("Fiona" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple2) -> rule4))]
("Erin" "is" "blue" "-")
((triple2) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
True
3
proof
[(((((triple2) -> rule4)) -> rule7))]
("Erin" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Fiona is not blue.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule4))]
("Fiona" "is" "blue" "-")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is green.
Unknown
rconc
[@5: Charlie is green.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule4 <- rule2 <- rule8 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not blue.
Unknown
inv-rconc
[@3: Charlie is blue.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule7 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Charlie is big.[(triple1)] Erin is green.[(triple2)] Fiona is quiet.[(triple3)] @1: Erin is blue.[(((triple2) -> rule4))] Fiona is cold.[(((triple3) -> rule3))] Fiona is green.[(((triple3) -> rule5))] @2: Erin is nice.[(((((triple2) -> rule4)) -> rule7))] Fiona is blue.[(((((triple3) -> rule5)) -> rule4))] @3: Fiona is big.[(((((((triple3) -> rule5)) -> rule4) ((triple3) -> rule3)) -> rule6))] Fiona is nice.[(((((((triple3) -> rule5)) -> rule4)) -> rule7) OR ((triple3 ((((triple3) -> rule5)) -> rule4)) -> rule8))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple3) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple3) -> (rule5 % int4))) -> (rule4 % int3)) ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
((triple3 ((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3