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