Bob is big. Bob is nice. Bob is smart. Bob is young. Charlie is not cold. Charlie is red. Charlie is smart. All red people are big. All young people are not cold. If Charlie is green and Charlie is big then Charlie is nice. Nice people are smart. All nice people are smart. If someone is big and not cold then they are green.
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
All young people are not cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "-"))
If Charlie is green and Charlie is big then Charlie is nice.
((("Charlie" "is" "green" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "nice" "+"))
Nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
All nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is big and not cold then they are green.
((("someone" "is" "big" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "green" "+"))
Charlie is red.
True
1
proof
[(triple6)]
("Charlie" "is" "red" "+")
triple6
Charlie is not red.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "red" "-")
triple6
Charlie is big.
True
2
proof
[(((triple6) -> rule1))]
("Charlie" "is" "big" "+")
((triple6) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Bob is cold.
False
2
inv-proof
[(((triple4) -> rule2))]
("Bob" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is green.
True
4
proof
[(((triple1 ((triple4) -> rule2)) -> rule6))]
("Bob" "is" "green" "+")
((triple1 ((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not cold.
("Bob" "is" "cold" "-")
int2
Bob is not green.
False
4
inv-proof
[(((triple1 ((triple4) -> rule2)) -> rule6))]
("Bob" "is" "green" "-")
((triple1 ((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not cold.
("Bob" "is" "cold" "-")
int2
Charlie is nice.
True
7
proof
[(((((((triple6) -> rule1) triple5) -> rule6) ((triple6) -> rule1)) -> rule3))]
("Charlie" "is" "nice" "+")
((((((triple6) -> (rule1 % int3)) triple5) -> (rule6 % int2)) ((triple6) -> (rule1 % int3))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not nice.
False
7
inv-proof
[(((((((triple6) -> rule1) triple5) -> rule6) ((triple6) -> rule1)) -> rule3))]
("Charlie" "is" "nice" "-")
((((((triple6) -> (rule1 % int3)) triple5) -> (rule6 % int2)) ((triple6) -> (rule1 % int3))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is big.[(triple1)] Bob is nice.[(triple2)] Bob is smart.[(triple3 OR ((triple2) -> rule4) OR ((triple2) -> rule5))] Bob is young.[(triple4)] Charlie is not cold.[(triple5)] Charlie is red.[(triple6)] Charlie is smart.[(triple7 OR ((((((((triple6) -> rule1) triple5) -> rule6) ((triple6) -> rule1)) -> rule3)) -> rule4) OR ((((((((triple6) -> rule1) triple5) -> rule6) ((triple6) -> rule1)) -> rule3)) -> rule5))] @1: Bob is not cold.[(((triple4) -> rule2))] Charlie is big.[(((triple6) -> rule1))] @2: Bob is green.[(((triple1 ((triple4) -> rule2)) -> rule6))] Charlie is green.[(((((triple6) -> rule1) triple5) -> rule6))] @3: Charlie is nice.[(((((((triple6) -> rule1) triple5) -> rule6) ((triple6) -> rule1)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple2) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple4
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
((((((((triple6) -> (rule1 % int4)) triple5) -> (rule6 % int3)) ((triple6) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
((((((((triple6) -> (rule1 % int4)) triple5) -> (rule6 % int3)) ((triple6) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Bob is not cold.
("Bob" "is" "cold" "-")
((triple4) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple6) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple1 ((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not cold.
("Bob" "is" "cold" "-")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((triple6) -> (rule1 % int2)) triple5) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple6) -> (rule1 % int3)) triple5) -> (rule6 % int2)) ((triple6) -> (rule1 % int3))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3