Dave is nice. Gary is green. Gary is young. If someone is rough then they are cold. If someone is cold then they are young. All rough people are round. Green people are nice. All young people are cold. All nice, green people are round. If someone is green and young then they are quiet. If Dave is green then Dave is nice.
Dave is nice.
("Dave" "is" "nice" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold then they are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
All nice, green people are round.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is green and young then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is green then Dave is nice.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "nice" "+"))
Gary is young.
True
1
proof
[(triple3)]
("Gary" "is" "young" "+")
triple3
Dave is not nice.
False
1
inv-proof
[(triple1)]
("Dave" "is" "nice" "-")
triple1
Gary is cold.
True
2
proof
[(((triple3) -> rule5))]
("Gary" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple2) -> rule4))]
("Gary" "is" "nice" "-")
((triple2) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "quiet" "-")
Dave is cold.
Unknown
rconc
[@3: Dave is cold.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule1 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Dave is nice.[(triple1)] Gary is green.[(triple2)] Gary is young.[(triple3)] @1: Gary is cold.[(((triple3) -> rule5))] Gary is nice.[(((triple2) -> rule4))] Gary is quiet.[(((triple2 triple3) -> rule7))] @2: Gary is round.[(((((triple2) -> rule4) triple2) -> rule6))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Gary is green.
("Gary" "is" "green" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple2 triple3) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2