Anne is blue. Fiona is rough. Harry is blue. If Harry is nice and Harry is cold then Harry is green. All rough people are nice. If Fiona is blue and Fiona is green then Fiona is nice. If Harry is red and Harry is green then Harry is big. All rough people are big. If Fiona is rough and Fiona is nice then Fiona is green. All red, blue people are big. All blue people are rough.
Anne is blue.
("Anne" "is" "blue" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If Harry is nice and Harry is cold then Harry is green.
((("Harry" "is" "nice" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "green" "+"))
All rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If Fiona is blue and Fiona is green then Fiona is nice.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "green" "+")) -> ("Fiona" "is" "nice" "+"))
If Harry is red and Harry is green then Harry is big.
((("Harry" "is" "red" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "big" "+"))
All rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If Fiona is rough and Fiona is nice then Fiona is green.
((("Fiona" "is" "rough" "+") ("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "green" "+"))
All red, blue people are big.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
All blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Harry is blue.
True
1
proof
[(triple3)]
("Harry" "is" "blue" "+")
triple3
Harry is not blue.
False
1
inv-proof
[(triple3)]
("Harry" "is" "blue" "-")
triple3
Fiona is big.
True
2
proof
[(((triple2) -> rule5))]
("Fiona" "is" "big" "+")
((triple2) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not big.
False
2
inv-proof
[(((triple2) -> rule5))]
("Fiona" "is" "big" "-")
((triple2) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Anne is nice.
True
3
proof
[(((((triple1) -> rule8)) -> rule2))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Harry is not big.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule5))]
("Harry" "is" "big" "-")
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "green" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is blue.[(triple1)] Fiona is rough.[(triple2)] Harry is blue.[(triple3)] @1: Anne is rough.[(((triple1) -> rule8))] Fiona is big.[(((triple2) -> rule5))] Fiona is nice.[(((triple2) -> rule2))] Harry is rough.[(((triple3) -> rule8))] @2: Anne is big.[(((((triple1) -> rule8)) -> rule5))] Anne is nice.[(((((triple1) -> rule8)) -> rule2))] Fiona is green.[(((triple2 ((triple2) -> rule2)) -> rule6))] Harry is big.[(((((triple3) -> rule8)) -> rule5))] Harry is nice.[(((((triple3) -> rule8)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple2) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple3) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2