Bob is green. Charlie is green. Charlie is kind. Charlie is nice. Charlie is rough. Dave is blue. Dave is furry. Dave is kind. Dave is rough. Fiona is furry. Fiona is kind. Fiona is rough. All nice things are green. Blue things are furry. All rough things are blue.
Bob is green.
("Bob" "is" "green" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
All nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
All rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Fiona is furry.
True
1
proof
[(triple10 OR ((((triple12) -> rule3)) -> rule2))]
("Fiona" "is" "furry" "+")
triple10
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Dave is not blue.
False
1
inv-proof
[(triple6 OR ((triple9) -> rule3))]
("Dave" "is" "blue" "-")
triple6
((triple9) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Fiona is blue.
True
2
proof
[(((triple12) -> rule3))]
("Fiona" "is" "blue" "+")
((triple12) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is not blue.
False
2
inv-proof
[(((triple12) -> rule3))]
("Fiona" "is" "blue" "-")
((triple12) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Charlie is furry.
True
3
proof
[(((((triple5) -> rule3)) -> rule2))]
("Charlie" "is" "furry" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not furry.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule2))]
("Charlie" "is" "furry" "-")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is furry.
Unknown
rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Bob" "is" "furry" "+")
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is green.[(triple1)] Charlie is green.[(triple2 OR ((triple4) -> rule1))] Charlie is kind.[(triple3)] Charlie is nice.[(triple4)] Charlie is rough.[(triple5)] Dave is blue.[(triple6 OR ((triple9) -> rule3))] Dave is furry.[(triple7 OR ((triple6) -> rule2) OR ((((triple9) -> rule3)) -> rule2))] Dave is kind.[(triple8)] Dave is rough.[(triple9)] Fiona is furry.[(triple10 OR ((((triple12) -> rule3)) -> rule2))] Fiona is kind.[(triple11)] Fiona is rough.[(triple12)] @1: Charlie is blue.[(((triple5) -> rule3))] Fiona is blue.[(((triple12) -> rule3))] @2: Charlie is furry.[(((((triple5) -> rule3)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((triple4) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
((triple9) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple7
((triple6) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Fiona is furry.
("Fiona" "is" "furry" "+")
triple10
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple11
Fiona is rough.
("Fiona" "is" "rough" "+")
triple12
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple5) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple12) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2