Bob is big. Bob is green. Bob is smart. Bob is white. Charlie is green. Charlie is nice. Charlie is rough. Charlie is smart. Dave is cold. Dave is nice. Dave is rough. Dave is smart. If something is rough then it is big. Green, cold things are white. If something is green then it is smart. White, smart things are nice. All big, green things are white. If Bob is nice then Bob is smart. Big things are rough. All smart, white things are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Green, cold things are white.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is green then it is smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
White, smart things are nice.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
All big, green things are white.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If Bob is nice then Bob is smart.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "smart" "+"))
Big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All smart, white things are big.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Dave is rough.
True
1
proof
[(triple11)]
("Dave" "is" "rough" "+")
triple11
Bob is not green.
False
1
inv-proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Charlie is big.
True
2
proof
[(((triple7) -> rule1))]
("Charlie" "is" "big" "+")
((triple7) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple11) -> rule1))]
("Dave" "is" "big" "-")
((triple11) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Bob is big.[(triple1 OR ((triple3 triple4) -> rule8) OR ((((triple2) -> rule3) triple4) -> rule8))] Bob is green.[(triple2)] Bob is smart.[(triple3 OR ((triple2) -> rule3))] Bob is white.[(triple4 OR ((triple1 triple2) -> rule5))] Charlie is green.[(triple5)] Charlie is nice.[(triple6 OR ((((((triple7) -> rule1) triple5) -> rule5) triple8) -> rule4) OR ((((((triple7) -> rule1) triple5) -> rule5) ((triple5) -> rule3)) -> rule4))] Charlie is rough.[(triple7)] Charlie is smart.[(triple8 OR ((triple5) -> rule3))] Dave is cold.[(triple9)] Dave is nice.[(triple10)] Dave is rough.[(triple11)] Dave is smart.[(triple12)] @1: Bob is nice.[(((triple4 triple3) -> rule4) OR ((triple4 ((triple2) -> rule3)) -> rule4) OR ((((triple1 triple2) -> rule5) triple3) -> rule4) OR ((((triple1 triple2) -> rule5) ((triple2) -> rule3)) -> rule4))] Bob is rough.[(((triple1) -> rule7) OR ((((triple3 triple4) -> rule8)) -> rule7) OR ((((((triple2) -> rule3) triple4) -> rule8)) -> rule7))] Charlie is big.[(((triple7) -> rule1))] Dave is big.[(((triple11) -> rule1))] @2: Charlie is white.[(((((triple7) -> rule1) triple5) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3 triple4) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple2) -> (rule3 % int2)) triple4) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((triple2) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple4
((triple1 triple2) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
((((((triple7) -> (rule1 % int3)) triple5) -> (rule5 % int2)) triple8) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple7) -> (rule1 % int4)) triple5) -> (rule5 % int3)) ((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
((triple5) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple9
Dave is nice.
("Dave" "is" "nice" "+")
triple10
Dave is rough.
("Dave" "is" "rough" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple12
Bob is nice.
("Bob" "is" "nice" "+")
((triple4 triple3) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple4 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple1 triple2) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple1 triple2) -> (rule5 % int3)) ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple3 triple4) -> (rule8 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((((triple2) -> (rule3 % int3)) triple4) -> (rule8 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
((triple7) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple11) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple7) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2