Bob is big. Bob is nice. Bob is quiet. Bob is smart. Charlie is nice. Charlie is quiet. Fiona is big. Fiona is quiet. Harry is furry. Harry is nice. Harry is quiet. Harry is red. All blue things are big. All big things are quiet. All nice things are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Fiona is big.
True
1
proof
[(triple7)]
("Fiona" "is" "big" "+")
triple7
Bob is not big.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule3))]
("Bob" "is" "big" "-")
triple1
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Bob is big.[(triple1 OR ((triple2) -> rule3))] Bob is nice.[(triple2)] Bob is quiet.[(triple3 OR ((triple1) -> rule2) OR ((((triple2) -> rule3)) -> rule2))] Bob is smart.[(triple4)] Charlie is nice.[(triple5)] Charlie is quiet.[(triple6 OR ((((triple5) -> rule3)) -> rule2))] Fiona is big.[(triple7)] Fiona is quiet.[(triple8 OR ((triple7) -> rule2))] Harry is furry.[(triple9)] Harry is nice.[(triple10)] Harry is quiet.[(triple11 OR ((((triple10) -> rule3)) -> rule2))] Harry is red.[(triple12)] @1: Charlie is big.[(((triple5) -> rule3))] Harry is big.[(((triple10) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple1) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
triple7
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
((triple7) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple12
Charlie is big.
("Charlie" "is" "big" "+")
((triple5) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple10) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1