Dave is not cold. Dave is rough. Dave is round. All rough things are not cold. All round, kind things are big. If something is rough then it is kind. If something is big and not cold then it is kind. If something is quiet and not cold then it is nice. If something is cold and not rough then it is nice.
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
All rough things are not cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "-"))
All round, kind things are big.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If something is rough then it is kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is big and not cold then it is kind.
((("something" "is" "big" "+") ("something" "is" "cold" "~")) -> ("something" "is" "kind" "+"))
If something is quiet and not cold then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "cold" "~")) -> ("something" "is" "nice" "+"))
If something is cold and not rough then it is nice.
((("something" "is" "cold" "+") ("something" "is" "rough" "~")) -> ("something" "is" "nice" "+"))
Dave is round.
True
1
proof
[(triple3)]
("Dave" "is" "round" "+")
triple3
Dave is cold.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule1))]
("Dave" "is" "cold" "+")
triple1
((triple2) -> (rule1 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is kind.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
True
4
proof
[(((triple3 ((triple2) -> rule3)) -> rule2))]
("Dave" "is" "big" "+")
((triple3 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not big.
False
4
inv-proof
[(((triple3 ((triple2) -> rule3)) -> rule2))]
("Dave" "is" "big" "-")
((triple3 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is not cold.[(triple1 OR ((triple2) -> rule1))] Dave is rough.[(triple2)] Dave is round.[(triple3)] @1: Dave is kind.[(((triple2) -> rule3))] @2: Dave is big.[(((triple3 ((triple2) -> rule3)) -> rule2))]
Dave is not cold.
("Dave" "is" "cold" "-")
triple1
((triple2) -> (rule1 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple3 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2