Bob is big. Bob is not furry. Bob is nice. Bob is round. Bob is smart. Charlie is red. Charlie is rough. Charlie is round. Charlie is not smart. Erin is big. Erin is not furry. Erin is not nice. Erin is red. Erin is not rough. Erin is round. Erin is smart. Nice, smart things are big. If something is nice then it is round. If Erin is not nice then Erin is red. If something is round then it is not furry. If Erin is furry and Erin is round then Erin is smart. If something is red and not big then it is rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Erin is big.
("Erin" "is" "big" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Nice, smart things are big.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is nice then it is round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If Erin is not nice then Erin is red.
((("Erin" "is" "nice" "~")) -> ("Erin" "is" "red" "+"))
If something is round then it is not furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "-"))
If Erin is furry and Erin is round then Erin is smart.
((("Erin" "is" "furry" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "smart" "+"))
If something is red and not big then it is rough.
((("something" "is" "red" "+") ("something" "is" "big" "~")) -> ("something" "is" "rough" "+"))
Charlie is red.
True
1
proof
[(triple6)]
("Charlie" "is" "red" "+")
triple6
Bob is furry.
False
1
inv-proof
[(triple2 OR ((triple4) -> rule4) OR ((((triple3) -> rule2)) -> rule4))]
("Bob" "is" "furry" "+")
triple2
((triple4) -> (rule4 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Charlie is not furry.
True
2
proof
[(((triple8) -> rule4))]
("Charlie" "is" "furry" "-")
((triple8) -> (rule4 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is furry.
False
2
inv-proof
[(((triple8) -> rule4))]
("Charlie" "is" "furry" "+")
((triple8) -> (rule4 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "rough" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is big.[(triple1 OR ((triple3 triple5) -> rule1))] Bob is nice.[(triple3)] Bob is not furry.[(triple2 OR ((triple4) -> rule4) OR ((((triple3) -> rule2)) -> rule4))] Bob is round.[(triple4 OR ((triple3) -> rule2))] Bob is smart.[(triple5)] Charlie is not smart.[(triple9)] Charlie is red.[(triple6)] Charlie is rough.[(triple7)] Charlie is round.[(triple8)] Erin is big.[(triple10)] Erin is not furry.[(triple11 OR ((triple15) -> rule4))] Erin is not nice.[(triple12)] Erin is not rough.[(triple14)] Erin is red.[(triple13 OR ((triple12) -> rule3))] Erin is round.[(triple15)] Erin is smart.[(triple16)] @1: Charlie is not furry.[(((triple8) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3 triple5) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not furry.
("Bob" "is" "furry" "-")
triple2
((triple4) -> (rule4 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple4
((triple3) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
triple8
Erin is big.
("Erin" "is" "big" "+")
triple10
Erin is not furry.
("Erin" "is" "furry" "-")
triple11
((triple15) -> (rule4 % int1))
Erin is not furry.
("Erin" "is" "furry" "-")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
triple12
Erin is not rough.
("Erin" "is" "rough" "-")
triple14
Erin is red.
("Erin" "is" "red" "+")
triple13
((triple12) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple15
Erin is smart.
("Erin" "is" "smart" "+")
triple16
Charlie is not furry.
("Charlie" "is" "furry" "-")
((triple8) -> (rule4 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1