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