Anne is red. Bob is kind. Charlie is green. Dave is smart. If Charlie is red and Charlie is kind then Charlie is big. All kind, red things are big. If something is big then it is rough. Kind, green things are big. All red, blue things are smart. All green things are red. All kind things are green. All big things are red.
Anne is red.
("Anne" "is" "red" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If Charlie is red and Charlie is kind then Charlie is big.
((("Charlie" "is" "red" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "big" "+"))
All kind, red things are big.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is big then it is rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Kind, green things are big.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
All red, blue things are smart.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Dave is smart.
True
1
proof
[(triple4)]
("Dave" "is" "smart" "+")
triple4
Bob is not kind.
False
1
inv-proof
[(triple2)]
("Bob" "is" "kind" "-")
triple2
Charlie is red.
True
2
proof
[(((triple3) -> rule6))]
("Charlie" "is" "red" "+")
((triple3) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple3) -> rule6))]
("Charlie" "is" "red" "-")
((triple3) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Bob is red.
True
3
proof
[(((((triple2) -> rule7)) -> rule6) OR ((((triple2 ((triple2) -> rule7)) -> rule4)) -> rule8))]
("Bob" "is" "red" "+")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not red.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule6) OR ((((triple2 ((triple2) -> rule7)) -> rule4)) -> rule8))]
("Bob" "is" "red" "-")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is rough.
True
5
proof
[(((((triple2 ((triple2) -> rule7)) -> rule4)) -> rule3) OR ((((triple2 ((((triple2) -> rule7)) -> rule6)) -> rule2)) -> rule3))]
("Bob" "is" "rough" "+")
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple2 ((((triple2) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is not rough.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule7)) -> rule4)) -> rule3) OR ((((triple2 ((((triple2) -> rule7)) -> rule6)) -> rule2)) -> rule3))]
("Bob" "is" "rough" "-")
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple2 ((((triple2) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "big" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "green" "-")
Dave is red.
Unknown
rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Dave" "is" "red" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is red.[(triple1)] Bob is kind.[(triple2)] Charlie is green.[(triple3)] Dave is smart.[(triple4)] @1: Bob is green.[(((triple2) -> rule7))] Charlie is red.[(((triple3) -> rule6))] @2: Bob is big.[(((triple2 ((triple2) -> rule7)) -> rule4) OR ((triple2 ((((triple2) -> rule7)) -> rule6)) -> rule2))] Bob is red.[(((((triple2) -> rule7)) -> rule6) OR ((((triple2 ((triple2) -> rule7)) -> rule4)) -> rule8))] @3: Bob is rough.[(((((triple2 ((triple2) -> rule7)) -> rule4)) -> rule3) OR ((((triple2 ((((triple2) -> rule7)) -> rule6)) -> rule2)) -> rule3))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple3) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple2 ((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((triple2 ((((triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple2 ((((triple2) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4