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