Anne is blue. Charlie is red. Dave is rough. Erin is red. Red people are round. All rough, quiet people are round. All red, quiet people are young. Red people are round. All rough people are red. If Anne is blue then Anne is red. All green people are quiet. Rough, green people are young.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is red.
("Erin" "is" "red" "+")
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
All rough, quiet people are round.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
All red, quiet people are young.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
All rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If Anne is blue then Anne is red.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "red" "+"))
All green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Rough, green people are young.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Dave is rough.
True
1
proof
[(triple3)]
("Dave" "is" "rough" "+")
triple3
Dave is not rough.
False
1
inv-proof
[(triple3)]
("Dave" "is" "rough" "-")
triple3
Charlie is round.
True
2
proof
[(((triple2) -> rule1) OR ((triple2) -> rule4))]
("Charlie" "is" "round" "+")
((triple2) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple2) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple3) -> rule5))]
("Dave" "is" "red" "-")
((triple3) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Anne is round.
True
3
proof
[(((((triple1) -> rule6)) -> rule1) OR ((((triple1) -> rule6)) -> rule4))]
("Anne" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Dave is not round.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule1) OR ((((triple3) -> rule5)) -> rule4))]
("Dave" "is" "round" "-")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "quiet" "-")
Anne is young.
Unknown
rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("Anne" "is" "young" "+")
Erin is not young.
Unknown
inv-rconc
[@2: Erin is young.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("Erin" "is" "young" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is blue.[(triple1)] Charlie is red.[(triple2)] Dave is rough.[(triple3)] Erin is red.[(triple4)] @1: Anne is red.[(((triple1) -> rule6))] Charlie is round.[(((triple2) -> rule1) OR ((triple2) -> rule4))] Dave is red.[(((triple3) -> rule5))] Erin is round.[(((triple4) -> rule1) OR ((triple4) -> rule4))] @2: Anne is round.[(((((triple1) -> rule6)) -> rule1) OR ((((triple1) -> rule6)) -> rule4))] Dave is round.[(((((triple3) -> rule5)) -> rule1) OR ((((triple3) -> rule5)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple2) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple2) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple4) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple4) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2