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