Anne is cold. Anne is kind. Anne is rough. Anne is round. Anne is smart. Anne is young. Charlie is young. Dave is cold. Dave is nice. Dave is rough. Dave is round. Dave is smart. If someone is rough then they are cold. All young people are smart.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
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 young.
("Charlie" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
All young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Dave is cold.
True
1
proof
[(triple8 OR ((triple10) -> rule1))]
("Dave" "is" "cold" "+")
triple8
((triple10) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Anne is not cold.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule1))]
("Anne" "is" "cold" "-")
triple1
((triple3) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is smart.
True
2
proof
[(((triple7) -> rule2))]
("Charlie" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple7) -> rule2))]
("Charlie" "is" "smart" "-")
((triple7) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is cold.[(triple1 OR ((triple3) -> rule1))] Anne is kind.[(triple2)] Anne is rough.[(triple3)] Anne is round.[(triple4)] Anne is smart.[(triple5 OR ((triple6) -> rule2))] Anne is young.[(triple6)] Charlie is young.[(triple7)] Dave is cold.[(triple8 OR ((triple10) -> rule1))] Dave is nice.[(triple9)] Dave is rough.[(triple10)] Dave is round.[(triple11)] Dave is smart.[(triple12)] @1: Charlie is smart.[(((triple7) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((triple3) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
((triple6) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
triple8
((triple10) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple9
Dave is rough.
("Dave" "is" "rough" "+")
triple10
Dave is round.
("Dave" "is" "round" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple12
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1