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