Bob is furry. Bob is rough. Bob is young. Erin is big. Erin is not furry. Erin is red. Erin is not rough. Erin is smart. Erin is white. Erin is young. Gary is not rough. Gary is white. If something is rough then it is big. If something is rough and white then it is young. If something is rough and not white then it is not furry. If Bob is big and Bob is rough then Bob is smart. Big things are smart. If something is young and not white then it is red. If something is smart and not rough then it is red. If Bob is not furry then Bob is big.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is white.
("Gary" "is" "white" "+")
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is rough and white then it is young.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is rough and not white then it is not furry.
((("something" "is" "rough" "+") ("something" "is" "white" "~")) -> ("something" "is" "furry" "-"))
If Bob is big and Bob is rough then Bob is smart.
((("Bob" "is" "big" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "smart" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is young and not white then it is red.
((("something" "is" "young" "+") ("something" "is" "white" "~")) -> ("something" "is" "red" "+"))
If something is smart and not rough then it is red.
((("something" "is" "smart" "+") ("something" "is" "rough" "~")) -> ("something" "is" "red" "+"))
If Bob is not furry then Bob is big.
((("Bob" "is" "furry" "~")) -> ("Bob" "is" "big" "+"))
Erin is young.
True
1
proof
[(triple10)]
("Erin" "is" "young" "+")
triple10
Erin is not white.
False
1
inv-proof
[(triple9)]
("Erin" "is" "white" "-")
triple9
Bob is big.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "big" "+")
((triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "big" "-")
((triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
True
3
proof
[(((((triple2) -> rule1)) -> rule5) OR ((((triple2) -> rule1) triple2) -> rule4))]
("Bob" "is" "smart" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5) OR ((((triple2) -> rule1) triple2) -> rule4))]
("Bob" "is" "smart" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "red" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "red" "+")
Gary is not smart.
Unknown
inv-rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Gary" "is" "smart" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is furry.[(triple1)] Bob is rough.[(triple2)] Bob is young.[(triple3)] Erin is big.[(triple4)] Erin is not furry.[(triple5)] Erin is not rough.[(triple7)] Erin is red.[(triple6 OR ((triple8 triple7) -> rule7) OR ((((triple4) -> rule5) triple7) -> rule7))] Erin is smart.[(triple8 OR ((triple4) -> rule5))] Erin is white.[(triple9)] Erin is young.[(triple10)] Gary is not rough.[(triple11)] Gary is white.[(triple12)] @1: Bob is big.[(((triple2) -> rule1))] @2: Bob is smart.[(((((triple2) -> rule1)) -> rule5) OR ((((triple2) -> rule1) triple2) -> rule4))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is not furry.
("Erin" "is" "furry" "-")
triple5
Erin is not rough.
("Erin" "is" "rough" "-")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple6
((triple8 triple7) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple4) -> (rule5 % int2)) triple7) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple8
((triple4) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
Gary is not rough.
("Gary" "is" "rough" "-")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2