Anne is blue. Anne is cold. Anne is quiet. Anne is rough. Anne is round. Anne is smart. Anne is young. Charlie is not blue. Charlie is cold. Charlie is quiet. Charlie is rough. Charlie is round. Charlie is smart. Charlie is young. Dave is not smart. Dave is young. If Anne is cold and Anne is smart then Anne is round. If someone is cold and not quiet then they are round. If someone is young and not smart then they are rough. If someone is quiet and not smart then they are rough. Cold people are young. Rough people are young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Dave is young.
("Dave" "is" "young" "+")
If Anne is cold and Anne is smart then Anne is round.
((("Anne" "is" "cold" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "round" "+"))
If someone is cold and not quiet then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "round" "+"))
If someone is young and not smart then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "rough" "+"))
If someone is quiet and not smart then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "rough" "+"))
Cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
Charlie is rough.
True
1
proof
[(triple11)]
("Charlie" "is" "rough" "+")
triple11
Charlie is not young.
False
1
inv-proof
[(triple14 OR ((triple11) -> rule6) OR ((triple9) -> rule5))]
("Charlie" "is" "young" "-")
triple14
((triple11) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple9) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is rough.
True
3
proof
[(((triple16 triple15) -> rule3))]
("Dave" "is" "rough" "+")
((triple16 triple15) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
3
inv-proof
[(((triple16 triple15) -> rule3))]
("Dave" "is" "rough" "-")
((triple16 triple15) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is quiet.[(triple3)] Anne is rough.[(triple4)] Anne is round.[(triple5 OR ((triple2 triple6) -> rule1))] Anne is smart.[(triple6)] Anne is young.[(triple7 OR ((triple2) -> rule5) OR ((triple4) -> rule6))] Charlie is cold.[(triple9)] Charlie is not blue.[(triple8)] Charlie is quiet.[(triple10)] Charlie is rough.[(triple11)] Charlie is round.[(triple12)] Charlie is smart.[(triple13)] Charlie is young.[(triple14 OR ((triple11) -> rule6) OR ((triple9) -> rule5))] Dave is not smart.[(triple15)] Dave is young.[(triple16)] @1: Dave is rough.[(((triple16 triple15) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple2 triple6) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple2) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple4) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple9
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple10
Charlie is rough.
("Charlie" "is" "rough" "+")
triple11
Charlie is round.
("Charlie" "is" "round" "+")
triple12
Charlie is smart.
("Charlie" "is" "smart" "+")
triple13
Charlie is young.
("Charlie" "is" "young" "+")
triple14
((triple11) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple9) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is not smart.
("Dave" "is" "smart" "-")
triple15
Dave is young.
("Dave" "is" "young" "+")
triple16
Dave is rough.
("Dave" "is" "rough" "+")
((triple16 triple15) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1