Anne is rough. Charlie is rough. Dave is quiet. Gary is green. If something is rough then it is round. If something is green and cold then it is furry. All round things are big. Furry, green things are round. If Dave is furry then Dave is rough. Round things are cold. Quiet, round things are big. All round, cold things are green.
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is green.
("Gary" "is" "green" "+")
If something is rough then it is round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is green and cold then it is furry.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Furry, green things are round.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If Dave is furry then Dave is rough.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "rough" "+"))
Round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Quiet, round things are big.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All round, cold things are green.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Dave is not quiet.
False
1
inv-proof
[(triple3)]
("Dave" "is" "quiet" "-")
triple3
Anne is round.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "-")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Dave is not furry.
Unknown
inv-rconc
[@4: Dave is furry.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule1 <- rule5 <- FAIL)]]
("Dave" "is" "furry" "-")
Gary is cold.
Unknown
rconc
[@3: Gary is cold.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule2 <- FAIL)]]
("Gary" "is" "cold" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Anne is rough.[(triple1)] Charlie is rough.[(triple2)] Dave is quiet.[(triple3)] Gary is green.[(triple4)] @1: Anne is round.[(((triple1) -> rule1))] Charlie is round.[(((triple2) -> rule1))] @2: Anne is big.[(((((triple1) -> rule1)) -> rule3))] Anne is cold.[(((((triple1) -> rule1)) -> rule6))] Charlie is big.[(((((triple2) -> rule1)) -> rule3))] Charlie is cold.[(((((triple2) -> rule1)) -> rule6))] @3: Anne is green.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule6)) -> rule8))] Charlie is green.[(((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule6)) -> rule8))] @4: Anne is furry.[(((((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule6)) -> rule8) ((((triple1) -> rule1)) -> rule6)) -> rule2))] Charlie is furry.[(((((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule6)) -> rule8) ((((triple2) -> rule1)) -> rule6)) -> rule2))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple2) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
((((((triple1) -> (rule1 % int4)) ((((triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule8 % int2)) ((((triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((triple2) -> (rule1 % int4)) ((((triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule8 % int2)) ((((triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4