Charlie is blue. Dave is kind. Fiona is cold. If someone is green then they are furry. Blue people are kind. If Fiona is cold then Fiona is blue. If someone is furry and blue then they are cold. All rough, blue people are cold. If Fiona is cold and Fiona is blue then Fiona is rough. All rough people are smart. If Charlie is blue and Charlie is green then Charlie is furry.
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
If someone is green then they are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If Fiona is cold then Fiona is blue.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "blue" "+"))
If someone is furry and blue then they are cold.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All rough, blue people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If Fiona is cold and Fiona is blue then Fiona is rough.
((("Fiona" "is" "cold" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "rough" "+"))
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is blue and Charlie is green then Charlie is furry.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "green" "+")) -> ("Charlie" "is" "furry" "+"))
Dave is kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "+")
triple2
Dave is not kind.
False
1
inv-proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
Fiona is blue.
True
2
proof
[(((triple3) -> rule3))]
("Fiona" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is not blue.
False
2
inv-proof
[(((triple3) -> rule3))]
("Fiona" "is" "blue" "-")
((triple3) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "smart" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Charlie is blue.[(triple1)] Dave is kind.[(triple2)] Fiona is cold.[(triple3)] @1: Charlie is kind.[(((triple1) -> rule2))] Fiona is blue.[(((triple3) -> rule3))] @2: Fiona is kind.[(((((triple3) -> rule3)) -> rule2))] Fiona is rough.[(((triple3 ((triple3) -> rule3)) -> rule6))] @3: Fiona is smart.[(((((triple3 ((triple3) -> rule3)) -> rule6)) -> rule7))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3