Charlie is furry. Charlie is quiet. Charlie is round. Charlie is white. Erin is furry. Erin is green. Erin is quiet. Erin is rough. Erin is round. Erin is smart. Fiona is furry. Fiona is green. Fiona is quiet. Fiona is rough. Fiona is smart. All white things are round. Rough things are green. If something is furry and quiet then it is rough.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
All white things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is furry and quiet then it is rough.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Charlie is furry.
True
1
proof
[(triple1)]
("Charlie" "is" "furry" "+")
triple1
Erin is not green.
False
1
inv-proof
[(triple6 OR ((triple8) -> rule2) OR ((((triple5 triple7) -> rule3)) -> rule2))]
("Erin" "is" "green" "-")
triple6
((triple8) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple5 triple7) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Charlie is rough.
True
3
proof
[(((triple1 triple2) -> rule3))]
("Charlie" "is" "rough" "+")
((triple1 triple2) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
3
inv-proof
[(((triple1 triple2) -> rule3))]
("Charlie" "is" "rough" "-")
((triple1 triple2) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
True
4
proof
[(((((triple1 triple2) -> rule3)) -> rule2))]
("Charlie" "is" "green" "+")
((((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not green.
False
4
inv-proof
[(((((triple1 triple2) -> rule3)) -> rule2))]
("Charlie" "is" "green" "-")
((((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "round" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Charlie is furry.[(triple1)] Charlie is quiet.[(triple2)] Charlie is round.[(triple3 OR ((triple4) -> rule1))] Charlie is white.[(triple4)] Erin is furry.[(triple5)] Erin is green.[(triple6 OR ((triple8) -> rule2) OR ((((triple5 triple7) -> rule3)) -> rule2))] Erin is quiet.[(triple7)] Erin is rough.[(triple8 OR ((triple5 triple7) -> rule3))] Erin is round.[(triple9)] Erin is smart.[(triple10)] Fiona is furry.[(triple11)] Fiona is green.[(triple12 OR ((triple14) -> rule2) OR ((((triple11 triple13) -> rule3)) -> rule2))] Fiona is quiet.[(triple13)] Fiona is rough.[(triple14 OR ((triple11 triple13) -> rule3))] Fiona is smart.[(triple15)] @1: Charlie is rough.[(((triple1 triple2) -> rule3))] @2: Charlie is green.[(((((triple1 triple2) -> rule3)) -> rule2))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
((triple4) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
((triple8) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple5 triple7) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple8
((triple5 triple7) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Fiona is furry.
("Fiona" "is" "furry" "+")
triple11
Fiona is green.
("Fiona" "is" "green" "+")
triple12
((triple14) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple11 triple13) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple13
Fiona is rough.
("Fiona" "is" "rough" "+")
triple14
((triple11 triple13) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple15
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1 triple2) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2