Charlie is quiet. Dave is nice. Dave is quiet. Dave is red. Dave is rough. Erin is blue. Erin is quiet. Erin is rough. Fiona is big. Fiona is blue. Fiona is quiet. Fiona is red. If someone is green then they are blue. If Erin is nice then Erin is not rough. All quiet people are rough. If someone is blue and big then they are green. If someone is green and red then they are big. If Charlie is rough then Charlie is green.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If Erin is nice then Erin is not rough.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "rough" "-"))
All quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue and big then they are green.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is green and red then they are big.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If Charlie is rough then Charlie is green.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "green" "+"))
Erin is blue.
True
1
proof
[(triple6)]
("Erin" "is" "blue" "+")
triple6
Dave is not red.
False
1
inv-proof
[(triple4)]
("Dave" "is" "red" "-")
triple4
Fiona is green.
True
3
proof
[(((triple10 triple9) -> rule4))]
("Fiona" "is" "green" "+")
((triple10 triple9) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not green.
False
3
inv-proof
[(((triple10 triple9) -> rule4))]
("Fiona" "is" "green" "-")
((triple10 triple9) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Charlie is green.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("Charlie" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("Charlie" "is" "green" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
True
4
proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule1))]
("Charlie" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not blue.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule1))]
("Charlie" "is" "blue" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Dave is not big.
Unknown
inv-rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is green.
Unknown
rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not blue.
Unknown
inv-rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Dave" "is" "blue" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "big" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Charlie is quiet.[(triple1)] Dave is nice.[(triple2)] Dave is quiet.[(triple3)] Dave is red.[(triple4)] Dave is rough.[(triple5 OR ((triple3) -> rule3))] Erin is blue.[(triple6)] Erin is quiet.[(triple7)] Erin is rough.[(triple8 OR ((triple7) -> rule3))] Fiona is big.[(triple9)] Fiona is blue.[(triple10)] Fiona is quiet.[(triple11)] Fiona is red.[(triple12)] @1: Charlie is rough.[(((triple1) -> rule3))] Fiona is green.[(((triple10 triple9) -> rule4))] Fiona is rough.[(((triple11) -> rule3))] @2: Charlie is green.[(((((triple1) -> rule3)) -> rule6))] @3: Charlie is blue.[(((((((triple1) -> rule3)) -> rule6)) -> rule1))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple3) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple8
((triple7) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple9
Fiona is blue.
("Fiona" "is" "blue" "+")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
Fiona is red.
("Fiona" "is" "red" "+")
triple12
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple10 triple9) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple11) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3