Anne is green. Anne is not nice. Bob is white. Dave is smart. Gary is big. Gary is cold. Gary is rough. Nice, white things are rough. If something is white and not smart then it is rough. All cold things are nice. All rough, green things are nice. If something is smart then it is nice. All smart, big things are cold. Nice things are white. If Anne is green and Anne is nice then Anne is rough. If something is rough then it is big.
Anne is green.
("Anne" "is" "green" "+")
Anne is not nice.
("Anne" "is" "nice" "-")
Bob is white.
("Bob" "is" "white" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Nice, white things are rough.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is white and not smart then it is rough.
((("something" "is" "white" "+") ("something" "is" "smart" "~")) -> ("something" "is" "rough" "+"))
All cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
All rough, green things are nice.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is smart then it is nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
All smart, big things are cold.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If Anne is green and Anne is nice then Anne is rough.
((("Anne" "is" "green" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "rough" "+"))
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Dave is smart.
True
1
proof
[(triple4)]
("Dave" "is" "smart" "+")
triple4
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Dave is nice.
True
2
proof
[(((triple4) -> rule5))]
("Dave" "is" "nice" "+")
((triple4) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple4) -> rule5))]
("Dave" "is" "nice" "-")
((triple4) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
True
3
proof
[(((((triple4) -> rule5)) -> rule7))]
("Dave" "is" "white" "+")
((((triple4) -> (rule5 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule7))]
("Gary" "is" "white" "-")
((((triple6) -> (rule3 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Dave is rough.
True
6
proof
[(((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1))]
("Dave" "is" "rough" "+")
((((triple4) -> (rule5 % int3)) ((((triple4) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not rough.
False
6
inv-proof
[(((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1))]
("Dave" "is" "rough" "-")
((((triple4) -> (rule5 % int3)) ((((triple4) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is big.
True
7
proof
[(((((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1)) -> rule9))]
("Dave" "is" "big" "+")
((((((triple4) -> (rule5 % int4)) ((((triple4) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is not big.
False
7
inv-proof
[(((((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1)) -> rule9))]
("Dave" "is" "big" "-")
((((((triple4) -> (rule5 % int4)) ((((triple4) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is cold.
True
9
proof
[(((triple4 ((((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1)) -> rule9)) -> rule6))]
("Dave" "is" "cold" "+")
((triple4 ((((((triple4) -> (rule5 % int5)) ((((triple4) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Dave is not cold.
False
9
inv-proof
[(((triple4 ((((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1)) -> rule9)) -> rule6))]
("Dave" "is" "cold" "-")
((triple4 ((((((triple4) -> (rule5 % int5)) ((((triple4) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "cold" "-")
Bob is big.
Unknown
rconc
[@4: Bob is big.[CWA. Example of deepest failure = (rule9 <- rule1 <- rule3 <- rule6 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "cold" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule9 <- rule1 <- FAIL)]]
("Anne" "is" "big" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Anne is green.[(triple1)] Anne is not nice.[(triple2)] Bob is white.[(triple3)] Dave is smart.[(triple4)] Gary is big.[(triple5 OR ((triple7) -> rule9) OR ((((((triple6) -> rule3) ((((triple6) -> rule3)) -> rule7)) -> rule1)) -> rule9))] Gary is cold.[(triple6)] Gary is rough.[(triple7 OR ((((triple6) -> rule3) ((((triple6) -> rule3)) -> rule7)) -> rule1))] @1: Dave is nice.[(((triple4) -> rule5))] Gary is nice.[(((triple6) -> rule3))] @2: Dave is white.[(((((triple4) -> rule5)) -> rule7))] Gary is white.[(((((triple6) -> rule3)) -> rule7))] @3: Dave is rough.[(((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1))] @4: Dave is big.[(((((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1)) -> rule9))] @5: Dave is cold.[(((triple4 ((((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1)) -> rule9)) -> rule6))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is not nice.
("Anne" "is" "nice" "-")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
((triple7) -> (rule9 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((((triple6) -> (rule3 % int4)) ((((triple6) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
((((triple6) -> (rule3 % int3)) ((((triple6) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((triple4) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple6) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple4) -> (rule5 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple6) -> (rule3 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple4) -> (rule5 % int3)) ((((triple4) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((((((triple4) -> (rule5 % int4)) ((((triple4) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
((triple4 ((((((triple4) -> (rule5 % int5)) ((((triple4) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5