Anne is green. Anne is not smart. Bob is blue. Bob is green. Bob is not rough. Bob is smart. Bob is young. Charlie is blue. Charlie is green. Charlie is red. Charlie is not rough. Charlie is round. Charlie is smart. Dave is blue. Dave is smart. If something is red and rough then it is green. Blue things are green. If something is round and red then it is young. If something is rough and not red then it is round. All red things are round. If Dave is red and Dave is smart then Dave is round. Blue, green things are not rough. If Anne is green and Anne is blue then Anne is not young.
Anne is green.
("Anne" "is" "green" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If something is red and rough then it is green.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is round and red then it is young.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is rough and not red then it is round.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "round" "+"))
All red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If Dave is red and Dave is smart then Dave is round.
((("Dave" "is" "red" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "round" "+"))
Blue, green things are not rough.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "-"))
If Anne is green and Anne is blue then Anne is not young.
((("Anne" "is" "green" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "young" "-"))
Bob is blue.
True
1
proof
[(triple3)]
("Bob" "is" "blue" "+")
triple3
Bob is not young.
False
1
inv-proof
[(triple7)]
("Bob" "is" "young" "-")
triple7
Charlie is young.
True
3
proof
[(((triple12 triple10) -> rule3) OR ((((triple10) -> rule5) triple10) -> rule3))]
("Charlie" "is" "young" "+")
((triple12 triple10) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple10) -> (rule5 % int2)) triple10) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((triple12 triple10) -> rule3) OR ((((triple10) -> rule5) triple10) -> rule3))]
("Charlie" "is" "young" "-")
((triple12 triple10) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple10) -> (rule5 % int2)) triple10) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Dave is not rough.
True
4
proof
[(((triple14 ((triple14) -> rule2)) -> rule7))]
("Dave" "is" "rough" "-")
((triple14 ((triple14) -> (rule2 % int2))) -> (rule7 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is rough.
False
4
inv-proof
[(((triple14 ((triple14) -> rule2)) -> rule7))]
("Dave" "is" "rough" "+")
((triple14 ((triple14) -> (rule2 % int2))) -> (rule7 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "round" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "round" "+")
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "young" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is green.[(triple1)] Anne is not smart.[(triple2)] Bob is blue.[(triple3)] Bob is green.[(triple4 OR ((triple3) -> rule2))] Bob is not rough.[(triple5 OR ((triple3 triple4) -> rule7) OR ((triple3 ((triple3) -> rule2)) -> rule7))] Bob is smart.[(triple6)] Bob is young.[(triple7)] Charlie is blue.[(triple8)] Charlie is green.[(triple9 OR ((triple8) -> rule2))] Charlie is not rough.[(triple11 OR ((triple8 triple9) -> rule7) OR ((triple8 ((triple8) -> rule2)) -> rule7))] Charlie is red.[(triple10)] Charlie is round.[(triple12 OR ((triple10) -> rule5))] Charlie is smart.[(triple13)] Dave is blue.[(triple14)] Dave is smart.[(triple15)] @1: Charlie is young.[(((triple12 triple10) -> rule3) OR ((((triple10) -> rule5) triple10) -> rule3))] Dave is green.[(((triple14) -> rule2))] @2: Dave is not rough.[(((triple14 ((triple14) -> rule2)) -> rule7))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is not smart.
("Anne" "is" "smart" "-")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
((triple3) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not rough.
("Bob" "is" "rough" "-")
triple5
((triple3 triple4) -> (rule7 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
((triple3 ((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is green.
("Charlie" "is" "green" "+")
triple9
((triple8) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple11
((triple8 triple9) -> (rule7 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
((triple8 ((triple8) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
triple10
Charlie is round.
("Charlie" "is" "round" "+")
triple12
((triple10) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple13
Dave is blue.
("Dave" "is" "blue" "+")
triple14
Dave is smart.
("Dave" "is" "smart" "+")
triple15
Charlie is young.
("Charlie" "is" "young" "+")
((triple12 triple10) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple10) -> (rule5 % int2)) triple10) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple14) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not rough.
("Dave" "is" "rough" "-")
((triple14 ((triple14) -> (rule2 % int2))) -> (rule7 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2