Anne is rough. Anne is young. Dave is big. Dave is not rough. Fiona is big. Fiona is green. Harry is cold. Harry is red. Harry is smart. Harry is young. If someone is young then they are smart. If Anne is smart and Anne is big then Anne is not young. If someone is red and not smart then they are not cold. Cold people are not green. If someone is cold then they are red. If Harry is rough and Harry is red then Harry is big.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is young then they are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
If Anne is smart and Anne is big then Anne is not young.
((("Anne" "is" "smart" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "young" "-"))
If someone is red and not smart then they are not cold.
((("someone" "is" "red" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "cold" "-"))
Cold people are not green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "-"))
If someone is cold then they are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If Harry is rough and Harry is red then Harry is big.
((("Harry" "is" "rough" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "big" "+"))
Harry is cold.
True
1
proof
[(triple7)]
("Harry" "is" "cold" "+")
triple7
Harry is not young.
False
1
inv-proof
[(triple10)]
("Harry" "is" "young" "-")
triple10
Harry is not green.
True
2
proof
[(((triple7) -> rule4))]
("Harry" "is" "green" "-")
((triple7) -> (rule4 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is green.
False
2
inv-proof
[(((triple7) -> rule4))]
("Harry" "is" "green" "+")
((triple7) -> (rule4 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "red" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "big" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Anne is rough.[(triple1)] Anne is young.[(triple2)] Dave is big.[(triple3)] Dave is not rough.[(triple4)] Fiona is big.[(triple5)] Fiona is green.[(triple6)] Harry is cold.[(triple7)] Harry is red.[(triple8 OR ((triple7) -> rule5))] Harry is smart.[(triple9 OR ((triple10) -> rule1))] Harry is young.[(triple10)] @1: Anne is smart.[(((triple2) -> rule1))] Harry is not green.[(((triple7) -> rule4))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is not rough.
("Dave" "is" "rough" "-")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is red.
("Harry" "is" "red" "+")
triple8
((triple7) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple9
((triple10) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple10
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is not green.
("Harry" "is" "green" "-")
((triple7) -> (rule4 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1