Bob is quiet. Bob is smart. Bob is young. Charlie is round. Charlie is white. Charlie is young. Dave is blue. Dave is round. Dave is white. Fiona is furry. Fiona is quiet. Fiona is smart. If someone is young and smart then they are blue. If Dave is young and Dave is furry then Dave is blue. All smart people are furry. If Charlie is blue and Charlie is furry then Charlie is white. All smart, young people are round. If someone is smart and round then they are blue. All quiet people are round. All round people are blue.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If someone is young and smart then they are blue.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If Dave is young and Dave is furry then Dave is blue.
((("Dave" "is" "young" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "blue" "+"))
All smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If Charlie is blue and Charlie is furry then Charlie is white.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "white" "+"))
All smart, young people are round.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is smart and round then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
All quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
All round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Bob is young.
True
1
proof
[(triple3)]
("Bob" "is" "young" "+")
triple3
Bob is not smart.
False
1
inv-proof
[(triple2)]
("Bob" "is" "smart" "-")
triple2
Bob is round.
True
2
proof
[(((triple1) -> rule7) OR ((triple2 triple3) -> rule5))]
("Bob" "is" "round" "+")
((triple1) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple2 triple3) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Fiona is not round.
False
2
inv-proof
[(((triple11) -> rule7))]
("Fiona" "is" "round" "-")
((triple11) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is blue.
True
3
proof
[(((((triple11) -> rule7)) -> rule8) OR ((triple12 ((triple11) -> rule7)) -> rule6))]
("Fiona" "is" "blue" "+")
((((triple11) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((triple12 ((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is not blue.
False
3
inv-proof
[(((((triple11) -> rule7)) -> rule8) OR ((triple12 ((triple11) -> rule7)) -> rule6))]
("Fiona" "is" "blue" "-")
((((triple11) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((triple12 ((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "furry" "-")
Charlie is furry.
Unknown
rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is quiet.[(triple1)] Bob is smart.[(triple2)] Bob is young.[(triple3)] Charlie is round.[(triple4)] Charlie is white.[(triple5)] Charlie is young.[(triple6)] Dave is blue.[(triple7 OR ((triple8) -> rule8))] Dave is round.[(triple8)] Dave is white.[(triple9)] Fiona is furry.[(triple10 OR ((triple12) -> rule3))] Fiona is quiet.[(triple11)] Fiona is smart.[(triple12)] @1: Bob is blue.[(((triple3 triple2) -> rule1) OR ((((triple1) -> rule7)) -> rule8) OR ((((triple2 triple3) -> rule5)) -> rule8) OR ((triple2 ((triple1) -> rule7)) -> rule6) OR ((triple2 ((triple2 triple3) -> rule5)) -> rule6))] Bob is furry.[(((triple2) -> rule3))] Bob is round.[(((triple1) -> rule7) OR ((triple2 triple3) -> rule5))] Charlie is blue.[(((triple4) -> rule8))] Fiona is round.[(((triple11) -> rule7))] @2: Fiona is blue.[(((((triple11) -> rule7)) -> rule8) OR ((triple12 ((triple11) -> rule7)) -> rule6))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Dave is blue.
("Dave" "is" "blue" "+")
triple7
((triple8) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple8
Dave is white.
("Dave" "is" "white" "+")
triple9
Fiona is furry.
("Fiona" "is" "furry" "+")
triple10
((triple12) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
Bob is blue.
("Bob" "is" "blue" "+")
((triple3 triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple2 triple3) -> (rule5 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple2 ((triple1) -> (rule7 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple2 ((triple2 triple3) -> (rule5 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple2 triple3) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple4) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple11) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple11) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((triple12 ((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2