Bob is big. Bob is blue. Bob is not quiet. Bob is not white. Bob is young. Fiona is not big. Fiona is blue. Fiona is nice. Fiona is white. Fiona is young. If Bob is young and Bob is blue then Bob is big. If something is white and not green then it is young. Big things are young. If Fiona is big then Fiona is young. Blue, green things are not big. All green things are not big. If something is big and young then it is nice. All nice things are blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is not white.
("Bob" "is" "white" "-")
Bob is young.
("Bob" "is" "young" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If Bob is young and Bob is blue then Bob is big.
((("Bob" "is" "young" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "big" "+"))
If something is white and not green then it is young.
((("something" "is" "white" "+") ("something" "is" "green" "~")) -> ("something" "is" "young" "+"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If Fiona is big then Fiona is young.
((("Fiona" "is" "big" "+")) -> ("Fiona" "is" "young" "+"))
Blue, green things are not big.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "-"))
All green things are not big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "-"))
If something is big and young then it is nice.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
All nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Fiona is not big.
True
1
proof
[(triple6)]
("Fiona" "is" "big" "-")
triple6
Bob is not blue.
False
1
inv-proof
[(triple2 OR ((((triple1 triple5) -> rule7)) -> rule8) OR ((((triple1 ((triple1) -> rule3)) -> rule7)) -> rule8))]
("Bob" "is" "blue" "-")
triple2
((((triple1 triple5) -> (rule7 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
True
3
proof
[(((triple1 triple5) -> rule7) OR ((triple1 ((triple1) -> rule3)) -> rule7) OR ((((triple5 triple2) -> rule1) triple5) -> rule7) OR ((((triple5 triple2) -> rule1) ((triple1) -> rule3)) -> rule7))]
("Bob" "is" "nice" "+")
((triple1 triple5) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple1 ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple5 triple2) -> (rule1 % int2)) triple5) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple5 triple2) -> (rule1 % int3)) ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not nice.
False
3
inv-proof
[(((triple1 triple5) -> rule7) OR ((triple1 ((triple1) -> rule3)) -> rule7) OR ((((triple5 triple2) -> rule1) triple5) -> rule7) OR ((((triple5 triple2) -> rule1) ((triple1) -> rule3)) -> rule7))]
("Bob" "is" "nice" "-")
((triple1 triple5) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple1 ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple5 triple2) -> (rule1 % int2)) triple5) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple5 triple2) -> (rule1 % int3)) ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Bob is big.[(triple1 OR ((triple5 triple2) -> rule1))] Bob is blue.[(triple2 OR ((((triple1 triple5) -> rule7)) -> rule8) OR ((((triple1 ((triple1) -> rule3)) -> rule7)) -> rule8))] Bob is not quiet.[(triple3)] Bob is not white.[(triple4)] Bob is young.[(triple5 OR ((triple1) -> rule3))] Fiona is blue.[(triple7 OR ((triple8) -> rule8))] Fiona is nice.[(triple8)] Fiona is not big.[(triple6)] Fiona is white.[(triple9)] Fiona is young.[(triple10)] @1: Bob is nice.[(((triple1 triple5) -> rule7) OR ((triple1 ((triple1) -> rule3)) -> rule7) OR ((((triple5 triple2) -> rule1) triple5) -> rule7) OR ((((triple5 triple2) -> rule1) ((triple1) -> rule3)) -> rule7))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple5 triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((((triple1 triple5) -> (rule7 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple3
Bob is not white.
("Bob" "is" "white" "-")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
((triple1) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
((triple8) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple8
Fiona is not big.
("Fiona" "is" "big" "-")
triple6
Fiona is white.
("Fiona" "is" "white" "+")
triple9
Fiona is young.
("Fiona" "is" "young" "+")
triple10
Bob is nice.
("Bob" "is" "nice" "+")
((triple1 triple5) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple1 ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple5 triple2) -> (rule1 % int2)) triple5) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple5 triple2) -> (rule1 % int3)) ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3